ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da). ecl-max(x)   

latex

Definitions	x:A. B(x), t  T, , ecl-max(x), x,y. t(x;y), AB, A, P  Q, False, x,y,z,w. t(x;y;z;w), x,y,z. t(x;y;z), x. t(x), x(s1,s2), x(s1,s2,s3,s4), x(s1,s2,s3), Prop, x(s)
Lemmas	ecl ind wf, nat wf, le wf, decl-state wf, ma-valtype wf, bool wf, Knd wf, ifthenelse wf, lt int wf, ecl wf, fpf wf, Id wf